A,B:Type, f:(AB), L:(A List), P:(Bprop{i:l}).
l_all(map(f; L); B; x.P(x))  l_all(L; A; x.P(f(x))) 

latex

Definitions	x:A. B(x), P  Q, P  Q, x(s), P  Q, P  Q, x:A. B(x), prop{i:l}, t  T
Lemmas	map wf, l member wf, iff wf